輪講 - 論理と計算のしくみ 5.3 型付きλ計算 (前半) (外部記事)
https://www.slideshare.net/oarat/53-56830331
#外部記事 
論理と計算のしくみ(本)
伊奈 林太郎
単純型付きλ計算の強正規可能性を示している
おれは面倒だったので単純型付きλ計算における値呼び簡約の停止性(値呼び簡約の停止性だけを示している)
教科書はこっちでやっており,強正規可能性は演習問題としている